NIL 
EVAL-AWAITS 
END 
  LE(X4,SUB1(J))  1 2
1 LE(X1,X1) AXIOM 21
2 LE(X1,X3) ¬LE(SUB1(J),X3) 3 4
3 LE(X1,X3) ¬LE(X2,THM20) ¬LE(SUB1(J),X3) 5 6
4 LE(U,THM20) AXIOM -15
5 LE(X1,X3) ¬LE(THM20,X5) ¬LE(X2,THM20) ¬LE(X5,X3) 7 8
6 LE(THM20,SUB1(J)) AXIOM -14
7 LE(A(X6),A(X4)) LE(X1,X3) ¬LE(X6,X5) ¬LE(X2,X6) ¬LE(X5,X3) AXIOM 13
8 ¬LE(A(THM20),A(J)) AXIOM -12

EVAL-AWAITS